Lean 4 基礎 - pogi-log

Lean 4 基礎

Lean 4のドキュメント

What is Lean - Lean Manual

Theorem Proving in Lean 4 - Theorem Proving in Lean 4

Theorem Proving in Lean 4 日本語訳 - Theorem Proving in Lean 4 日本語訳

証明を書くためのコマンドはタクティク(tactic)

intro

constructor

code:memo

-- 1行コメント

/-

複数行コメント

-/

#で始まるものは実行すると結果がすぐに確認できるようコマンドに分類される

こういうのは「対話的」とよばれる

code:memo

-- evalコマンド

#eval "Hello, World!"

--> "Hello, World!"

def double (x : Nat) : Nat :=

x + x

#eval double 3

--> 6

code:memo

-- #check コマンド

#check 2 + 2 = 4

--> 2 + 2 = 4 : Prop

code:memo

theorem easy : 2 + 2 = 4 :=

rfl

theorem hard : FermatLastTheorem :=

sorry

uは宇宙レベルを表す変数

rw

⊢

Goalが左辺=右辺なら証明完了

induction n with d hd

apply

含意 → をゴールに適用するタクティク

apply h2 at h1なら仮定h2を仮定h1に適用する

code:memo

h1: x = 37

h2: x = 37 → y = 42

↓ apply h2 at h1

h2: x = 37 → y = 42

h1: y = 42

apply succ_inj at hなら仮定hのsuccを除去する

succ(a) = succ(b)→a = b

code:memo

h: succ (succ 0) = succ (succ (succ 0))

↓ apply succ_inj at h

h: succ 0 = succ (succ 0)

apply succ_injならゴールに適用する

intro

intro hで仮定を作る？

exact

exact hで仮定をゴールを比較する

数学系のためのLean勉強会 - 数学系のためのLean勉強会

【Lean実況】数学系のためのLean勉強会の教材を解くBasic1 - YouTube

https://www.youtube.com/watch?v=1saX8G-wN2o&list=PL-2TwNpShL3yJRE2xUwOEujUv6j4S0_ml&index=1

確認用

Q. 1行コメント

Q. 複数行コメント

参考

依存型理論 - Theorem Proving in Lean 4 日本語訳

タクティク - Lean by Example

数学系のためのLean勉強会 - 数学系のためのLean勉強会

Leanのインストール・基礎

関連

単純型理論

依存型理論

Types as objects

Proj: Natural number gameを解く

メモ

GitHub: yuma-mizuno/lean-math-workshop: 数学系のためのLean勉強会

証明支援システムLeanに入門する #2

調査用

/pogi-log/Google.icon Lean 4 基礎